FDL - Nuprl Lemma : p-first-cons

Nuprl Lemma : p-first-cons

A, B:Type, L:((A

(B + Top)) List), f:(A

(B + Top)).
p-first([f / L]) = [f?p-first(L)]

A

(B + Top)

Definitions Top, left + right, x:AB(x), s = t, x:A. B(x), type List, Type, [], [car / cdr], as @ bs, s ~ t, t T, True, T, [f?g], P Q, P Q, x:A B(x), P & Q, P Q, p-first(L)

Lemmas p-first-singleton, p-first-append, p-conditional-to-p-first, p-conditional wf, squash wf, true wf, top wf